$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $C$:Type, $D$:($C$$\rightarrow$Type).
\\[0ex]$A$ $\subseteq\rho$ $C$ $\Rightarrow$ ($\forall$$a$:$A$. $B$($a$) $\subseteq\rho$ $D$($a$)) $\Rightarrow$ ($a$:$A$$\times$$B$($a$)) $\subseteq\rho$ ($c$:$C$$\times$$D$($c$))